structure VCptrans =
struct
  structure P = Proof
  structure VC = VC
  structure E = Env
  structure A = Assert
  structure S2C = Svc2avc
  structure T = Temp
  
  fun get_vc_proof svc label env senv infunc (st:A.state) =
      let val args = ref []
          val term = ref (P.ID(label))
          val _ = T.reset_var()
          fun getp (VC.Forall(id, tp, exp)) st =
              let val id_inf = E.lookup id env
              in  (case id_inf 
                    of  NONE => ()
                      | _ => let val (idexp, _, _) = S2C.transLval' (VC.Var(id)) infunc env senv st
                             in  term := P.Apply ((!term), P.Exp(idexp))
                             end);
                  getp exp st
              end 
            | getp (VC.Imply(exp1, exp2)) st =
              let val H1 = T.new_var() (*WIP*)
                  val H1exp = P.Prop(S2C.transProp' exp1 infunc env senv st)
              in  args := (H1, H1exp)::(!args);
                  term := P.Apply (!term, P.ID(H1));
                  getp exp2 st
              end
            | getp (VC.True) st = ()
            | getp (VC.False) st = ()
            | getp (VC.Not(e)) st = ()
            | getp (VC.BinopExp(e1, VC.Equ, e2)) st = ()
            | getp (VC.BinopExp(e1, VC.NEqu, e2)) st = ()
            | getp (VC.BinopExp(e1, VC.GT, e2)) st =()
            | getp (VC.BinopExp(e1, VC.GE, e2)) st =()
            | getp (VC.BinopExp(e1, VC.LT, e2)) st =()
            | getp (VC.BinopExp(e1, VC.LE, e2)) st =()
            | getp _ st = (raise Fail "impossible! must be prop~"; ())
          fun makefunc (arg, t) = P.Func(arg, t)     
      in  getp svc st;
          List.foldr makefunc (!term) (!args)
      end

end
